\begin{tabbing}
old\_event\_system\{i:l\}
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$E$:Type$_{\mbox{\scriptsize i}}$\+
\\[0ex]$\times$EqDecider($E$)
\\[0ex]$\times$$T$:(Id$\rightarrow$Id$\rightarrow$Type$_{\mbox{\scriptsize i}}$)
\\[0ex]$\times$$V$:(Id$\rightarrow$Id$\rightarrow$Type$_{\mbox{\scriptsize i}}$)
\\[0ex]$\times$$M$:(IdLnk$\rightarrow$Id$\rightarrow$Type$_{\mbox{\scriptsize i}}$)
\\[0ex]$\times$Top
\\[0ex]$\times$${\it loc}$:($E$$\rightarrow$Id)
\\[0ex]$\times$${\it kind}$:($E$$\rightarrow$Knd)
\\[0ex]$\times$${\it val}$:($e$:$E$$\rightarrow$eventtype(${\it kind}$;${\it loc}$;$V$;$M$;$e$))
\\[0ex]$\times$${\it when}$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow$$T$(${\it loc}$($e$),$x$))
\\[0ex]$\times$${\it after}$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow$$T$(${\it loc}$($e$),$x$))
\\[0ex]$\times$${\it sends}$:($l$:IdLnk$\rightarrow$$E$$\rightarrow$(Msg\_sub($l$;$M$) List))
\\[0ex]$\times$${\it sender}$:(\{$e$:$E$$\mid$ isrcv(${\it kind}$($e$)) \}$\rightarrow$$E$)
\\[0ex]$\times$${\it index}$:($e$:\{$e$:$E$$\mid$ isrcv(${\it kind}$($e$)) \}$\rightarrow$\{0..$\parallel$${\it sends}$(lnk(${\it kind}$($e$)),${\it sender}$($e$))$\parallel^{-}$\})
\\[0ex]$\times$${\it first}$:($E$$\rightarrow\mathbb{B}$)
\\[0ex]$\times$${\it pred}$:(\{${\it e'}$:$E$$\mid$ $\neg$${\it first}$(${\it e'}$) \}$\rightarrow$$E$)
\\[0ex]$\times$${\it causl}$:($E$$\rightarrow$$E$$\rightarrow$Prop$_{\mbox{\scriptsize i}}$)
\\[0ex]$\times$ESAxioms\=\{i:l\}\+
\\[0ex](\=$E$;\+
\\[0ex]$T$;
\\[0ex]$M$;
\\[0ex]${\it loc}$;
\\[0ex]${\it kind}$;
\\[0ex]${\it val}$;
\\[0ex]${\it when}$;
\\[0ex]${\it after}$;
\\[0ex]${\it sends}$;
\\[0ex]${\it sender}$;
\\[0ex]${\it index}$;
\\[0ex]${\it first}$;
\\[0ex]${\it pred}$;
\\[0ex]${\it causl}$)
\-\-\\[0ex]$\times$${\it Trans}$:($i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.$V$($i$,$a$); $l$,$t$.$M$($l$,$t$) )$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$($x$:Id$\rightarrow$\=$T$\+
\\[0ex]($i$
\\[0ex],$x$)))
\-\\[0ex]$\times$${\it Send}$:(\=$i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.$V$($i$,$a$); $l$,$t$.$M$($l$,$t$) )$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$\+
\\[0ex](Msg($M$) List))
\-\\[0ex]$\times$${\it Choose}$:($i$:Id$\rightarrow$$a$:Id$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$($V$($i$,$a$)+Unit))
\\[0ex]$\times$\=ESMachineAxiom($E$;$T$;$V$;$M$;${\it loc}$;${\it kind}$;${\it val}$;\+
\\[0ex]${\it when}$;${\it after}$;
\\[0ex]${\it sender}$;${\it Trans}$;${\it Send}$;${\it Choose}$)
\-\\[0ex]$\times$ESAtomAxiom\=\{i:l\}\+
\\[0ex]($T$; ($\lambda$$i$,$k$. kindcase($k$; $a$.$V$($i$,$a$); $l$,$t$.$M$($l$,$t$) )))
\-\\[0ex]$\times$Top
\-
\end{tabbing}